LeanGuard：面向工具调用智能体的 Lean 验证护栏
🧭 LLM Agent 形式化护栏与自动修复 ★ 深度解读
Case Western Reserve University · UT Austin
在 LLM 智能体与工具之间嵌入 Lean 4 策略运行时，以形式化证明保证每次工具调用合规，并支持反馈或证明引导修复
📌 工作参考价值（4 点）
- 在电商导购/售后 Agent 的写操作（改订单、退款、发券）上，可借鉴“外部策略运行时 + 可信证据”架构：把业务规则写成 permits/requirements/forbids，所有工具调用先做 fail-closed 校验；关键点是不信 LLM 输出的文本，只信后端快照和监控日志，用户确认绑定到具体提案和状态版本，防止注入礼品卡/收款账户等越权操作。
- 将拒绝从“调用未执行”改为“失败规则 + 修复提示”，可减少重复试错并提高恢复率；论文中反馈使阻塞调用从 983 降到 719，恢复动作从 34 增至 48。售后场景可返回具体缺失条件（如需先读订单、需用户确认）而非笼统拒绝。
- 证明引导修复对参数值类违规很实用：当金额超预算、支付方式不合规、选错券时，可在规则引擎中预计算最近合规参数并随拒绝返回，或直接替换；论文在 252 个参数值拒绝中证明修复 88 个，中位 2ms，表明部分修复不必让模型重试。
- 若业务涉及支付、退款、隐私等强保障环节，可考虑用可验证语言编写核心策略，并检查证明无 sorry/非标准公理；但维护成本高，适合核心高风险写操作而非全量策略。
自动化定理证明中的苦涩教训：简单 Agent 循环
🧭 Agent 自反思 + 形式化验证
FAIR at Meta · EPFL · CERMICS, ENPC, Institut Polytechnique de Paris · New York University
提出 h1，一个只靠高效 Lean 接口与验证反馈自反思的简单 agent 循环，在形式定理证明达到 SOTA 并追上复杂工作流
📌 工作参考价值（4 点）
- 构建 LLM agent 做 query 生成、推荐文案或策略搜索时，不要先上规划/多智能体分解；先用单 agent + 可执行验证器（搜索 API 结果、商品约束、SQL 执行）做自反思循环，用 pass@1/多采样衡量，效率和效果常超复杂编排。
- 工具/环境接口的反馈延迟与信息质量是关键：把验证器返回做成结构化、可增量复用（如错误位置、候选修正），减少模型盲目重试；类比 h1 的 Lean 4 增量编译与错误上下文。
- 做消融和 matched-model 对比：换更强模型或更多计算会混淆 workflow 收益；固定模型，对比简单 loop vs 复杂 agent 架构，避免苦涩教训。
- 如果业务里有可靠执行环境（规则校验、线上仿真、评分器），把计算预算花在多次验证反馈循环（test-time compute）上，可能比重构提示/工作流更划算。
Vero：AI Agent 能构建形式化验证的软件仓库吗
🧭 AI Agent 形式化验证代码生成基准
UC Berkeley · University of Chicago · California Institute of Technology · Stanford University · Amazon Web Services
首个仓库级实现与证明联合合成的形式化验证基准，当前最强 Agent 仅完全解决 27/43
📌 工作参考价值（4 点）
- 在电商/推荐系统的关键路径（如扣费、库存、ETL 数据一致性）中引入形式化验证 gate：为 API 接口编写 spec 和机器可检查证明，替代或补充单测，避免边界条件下的隐性 bug。
- 评估内部 AI coding agent 时，不要仅看测试通过率；可仿照 Vero 设计双模式评测：proof-only（只补证明）和 code-and-proof（实现+证明联合生成），衡量 agent 能否在多模块上下文中保持规范一致性。
- 采用 Vero 的审计机制：允许 agent 证明 spec 不可满足或参考实现错误，用于自动发现接口契约或参考代码中的隐含缺陷；迁移到业务中可对服务间契约建立形式化检查，提前暴露集成矛盾。
- 仓库级验证思维对微服务架构有参考意义：把跨服务数据流、状态迁移约束用 Lean 4 等语言形式化，不仅能保证单个模块正确，还能验证跨模块组合语义，适合交易链路等高可靠场景。